i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
update-spec-decl(upd; ds)
 msg-spec-loc-decl(snd; i; da)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 R-Feasible{i:l}
 R-Feasible(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd))
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:((decl-state(ds2)Tdecl-type{i:l}
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:((decl-state(ds2)Tdecl-type(ds2; x
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:((decl-state(ds2)Tdecl-type()) + (decl-state
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:((decl-state(ds2)Tdecl-type()) + ((ds2)
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:(Trationalsdecl-type{i:l}
 (k:Knd, ds2:fpf(Id; x.Type), T:Type, x:Id, f:(Trationalsdecl-type(ds2; x))).
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds2)))
  ((eq_id(mkid{ecl:ut2}; x)))
  fpf-compatible(Id; x.Type; id-deq; ds; ds2)
  fpf-compatible(Knd; k.Type; Kind-deq; da; fpf-single(k; T))
  ((k  ecl-kinds(A))  ((ma-valtype(da; k) = T)  (fpf-dom(Kind-deq; k; da))))
  ((x  update-spec-vars(upd)))
  R-compat{i:l}
  R-compat(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); Reffect(i; ds2; k; T; x; f))) 

latex

Definitions

let x = a in b(x), suptype(S; T), subtype(S; T), IdLnk, R-lnk-tags(ds; da; l; tgs; ks; g), ecl-machine3(ds; da; x; T; ks; a; snd), P  Q, x,y. t(x;y), fpf-cap(f; eq; x; z), False, A  B, x:A. B(x), (x  l), A, ecl-machine2(i; ds; da; x; T; ks; a; upd), ma-valtype(da; k), Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), guard(T), sq_type(T), Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), t.2, bor(p; q), t.1, (i = j), band(p; q), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), Y, ff, tt, if b then t else f fi , R-compat{i:l}(A; B), decl-type{i:l}(ds; x), decl-state(ds), Knd, P  Q, x. t(x), True, T, prop{i:l}, P  Q, ecl-trans-ks(v), R-state-var(i; ds; da; x; T; ks; tr), R-state-var-init(i; ds; da; x; T; v; ks; tr), A c B, t  T, top, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A), P  Q, ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), mkid{$x:ut2}, P  Q, Id, x:A. B(x), fpf-ap(f; eq; x), fpf-single(x; v), fpf-compatible(A; a.B(a); eq; f; g), x(s1,s2), update-spec(ds; da), , update-spec-decl(upd; ds), Unit, , b, ecl-trans-tuple{i:l}(ds; da), x(s), eq_id(a; b),

Lemmas

es-dt-dom, isrcv-implies, es-dt-ap, Rsframe wf, IdLnk sq, isrcv wf, eq lnk wf, tagof wf, lnk wf, assert-eq-lnk, lnk-decl-compatible-single, lnk-decl wf, lsrc wf, rcv wf, es-dt-cap, fpf-cap-void-subtype, es-dt wf, Rsends wf, ecl-m3 wf, ecl-tags wf, R-lnk-tags wf, msg-spec-links wf, idlnk-deq wf, remove-repeats wf, decl-state-subtype, fpf-single-dom, or functionality wrt iff, fpf-join-dom2, fpf-compatible-symmetry, fpf-cap-join-subtype, list accum wf, fpf-compatible-single-iff, select wf, length wf1, nat wf, fpf-ap wf, R-state-var wf, Knd sq, fpf-empty-compatible-left, eq id self, assert-eq-knd, eq knd wf, not functionality wrt iff, fpf-compatible-singles, fpf-compatible-single2, fpf-compatible-join2, Id sq, assert-eq-id, subtype rel self, fpf-sub weakening, fpf-single wf, fpf-sub-join-left2, subtype-fpf-cap-top, top wf, fpf-cap wf, subtype rel dep function, assert of bnot, eqff to assert, bnot wf, iff transitivity, eqtt to assert, bool wf, eqof eq btrue, fpf-cap-single, fpf-join-cap-sq, fpf-join wf, Reffect wf, IdLnk wf, R-compat-Rall2, ecl wf, msg-spec wf, update-spec wf, update-spec-decl wf, msg-spec-loc-decl wf, ecl-machine wf, R-Feasible wf, fpf wf, rationals wf, decl-type wf, decl-state wf, eq id wf, id-deq wf, fpf-single wf3, fpf-compatible wf, Kind-deq wf, ecl-kinds wf, Knd wf, update-spec-vars wf, Id wf, not wf, ecl-trans-tuple wf, ecl-trans wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, ma-valtype wf, ecl-kinds-ecl-trans, true wf, squash wf, l member wf, R-compat-Rplus-sq